(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2.
The certificate found is represented by the following graph.
Start state: 578
Accept states: [579]
Transitions:
578→579[0_1|0]
578→578[1_1|0, 2_1|0]
578→580[2_1|1]
578→589[2_1|1]
580→581[1_1|1]
581→582[0_1|1]
582→583[2_1|1]
583→584[1_1|1]
584→585[0_1|1]
585→586[1_1|1]
586→587[1_1|1]
587→588[2_1|1]
588→579[1_1|1]
588→582[1_1|1]
588→591[1_1|1]
588→601[2_1|2]
588→610[2_1|2]
589→590[1_1|1]
590→591[0_1|1]
591→592[2_1|1]
592→593[1_1|1]
593→594[0_1|1]
594→595[2_1|1]
595→596[1_1|1]
596→597[0_1|1]
597→598[1_1|1]
598→599[1_1|1]
599→600[2_1|1]
600→579[1_1|1]
600→582[1_1|1]
600→591[1_1|1]
600→601[2_1|2]
600→610[2_1|2]
601→602[1_1|2]
602→603[0_1|2]
603→604[2_1|2]
604→605[1_1|2]
605→606[0_1|2]
606→607[1_1|2]
607→608[1_1|2]
608→609[2_1|2]
609→585[1_1|2]
609→594[1_1|2]
609→622[2_1|2]
609→631[2_1|2]
610→611[1_1|2]
611→612[0_1|2]
612→613[2_1|2]
613→614[1_1|2]
614→615[0_1|2]
615→616[2_1|2]
616→617[1_1|2]
617→618[0_1|2]
618→619[1_1|2]
619→620[1_1|2]
620→621[2_1|2]
621→585[1_1|2]
621→594[1_1|2]
621→622[2_1|2]
621→631[2_1|2]
622→623[1_1|2]
623→624[0_1|2]
624→625[2_1|2]
625→626[1_1|2]
626→627[0_1|2]
627→628[1_1|2]
628→629[1_1|2]
629→630[2_1|2]
630→597[1_1|2]
631→632[1_1|2]
632→633[0_1|2]
633→634[2_1|2]
634→635[1_1|2]
635→636[0_1|2]
636→637[2_1|2]
637→638[1_1|2]
638→639[0_1|2]
639→640[1_1|2]
640→641[1_1|2]
641→642[2_1|2]
642→597[1_1|2]